$\forall$${\it es}$:ES, $i$, $x$:Id, $s_{1}$, $s_{2}$:($x$:Id$\rightarrow$vartype($i$;$x$)). $s_{1}$ $\equiv$ $s_{2}$ mod $x$@$i$ $\in$ Prop